| 1: | first(0,X) | → nil | |
| 2: | first(s(X),cons(Y,Z)) | → cons(Y,n__first(X,activate(Z))) | |
| 3: | from(X) | → cons(X,n__from(n__s(X))) | |
| 4: | first(X1,X2) | → n__first(X1,X2) | |
| 5: | from(X) | → n__from(X) | |
| 6: | s(X) | → n__s(X) | |
| 7: | activate(n__first(X1,X2)) | → first(activate(X1),activate(X2)) | |
| 8: | activate(n__from(X)) | → from(activate(X)) | |
| 9: | activate(n__s(X)) | → s(activate(X)) | |
| 10: | activate(X) | → X | |
| 11: | FIRST(s(X),cons(Y,Z)) | → ACTIVATE(Z) | |
| 12: | ACTIVATE(n__first(X1,X2)) | → FIRST(activate(X1),activate(X2)) | |
| 13: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X1) | |
| 14: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X2) | |
| 15: | ACTIVATE(n__from(X)) | → FROM(activate(X)) | |
| 16: | ACTIVATE(n__from(X)) | → ACTIVATE(X) | |
| 17: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 18: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |